Inference at * 
Iof proof for Lemma fun thru ite:


  S,T:Type, f:(ST), b:, p,q:S. f(if b then p else q fi ) = if b then f(p) else f(q) fi  

latex

 by ((((((RepD) 
CollapseTHENM (OnVar `b' BoolCases))) 
CollapseTHENM (AbReduce 0))) 

CoCollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t
C) inil_term))) 

latex

C.

Definitions	ff, tt, t  T, if b then t else f fi , x:A. B(x), Unit, ,
Lemmas	bool wf